Left Termination of the query pattern test_snake_in_3(g, g, g) w.r.t. the given Prolog program could not be shown:



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof

Clauses:

test_snake(Pattern, C, R) :- ','(s2l(C, Cols), ','(s2l(R, Rows), snake(Pattern, Cols, Rows))).
s2l(0, []).
s2l(s(X), .(X1, Y)) :- s2l(X, Y).
snake(Pattern, Cols, Rows) :- ','(infinite_snake(Pattern, InfSnake, InfSnake), ','(produce_snake(Rows, Cols, InfSnake, Snake), coil_it(Snake, odd))).
infinite_snake([], S, S).
infinite_snake(.(A, R), .(A, T), S) :- infinite_snake(R, T, S).
produce_snake([], X, X1, []).
produce_snake(.(X, Rows), Cols, InfSnake, .(Part, Tail)) :- ','(part_of_snake(Cols, InfSnake, NewInfSnake, Part), produce_snake(Rows, Cols, NewInfSnake, Tail)).
part_of_snake([], RestSnake, RestSnake, []).
part_of_snake(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) :- part_of_snake(R, Rings, RestSnake, RestRings).
coil_it([], X).
coil_it(.(Line, Lines), odd) :- coil_it(Lines, even).
coil_it(.(Line, Lines), even) :- ','(reverse2(Line, Line1), coil_it(Lines, odd)).
reverse2(List, Reversed) :- reverse(List, [], Reversed).
reverse([], Reversed, Reversed).
reverse(.(Head, Tail), SoFar, Reversed) :- reverse(Tail, .(Head, SoFar), Reversed).

Queries:

test_snake(g,g,g).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
test_snake_in: (b,b,b)
s2l_in: (b,f)
snake_in: (b,b,b)
infinite_snake_in: (b,f,f)
produce_snake_in: (b,b,f,f)
part_of_snake_in: (b,f,f,f)
coil_it_in: (b,b)
reverse2_in: (f,f)
reverse_in: (f,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
  ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

TEST_SNAKE_IN_GGG(Pattern, C, R) → U1_GGG(Pattern, C, R, s2l_in_ga(C, Cols))
TEST_SNAKE_IN_GGG(Pattern, C, R) → S2L_IN_GA(C, Cols)
S2L_IN_GA(s(X), .(X1, Y)) → U4_GA(X, X1, Y, s2l_in_ga(X, Y))
S2L_IN_GA(s(X), .(X1, Y)) → S2L_IN_GA(X, Y)
U1_GGG(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_GGG(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U1_GGG(Pattern, C, R, s2l_out_ga(C, Cols)) → S2L_IN_GA(R, Rows)
U2_GGG(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_GGG(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
U2_GGG(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → SNAKE_IN_GGG(Pattern, Cols, Rows)
SNAKE_IN_GGG(Pattern, Cols, Rows) → U5_GGG(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
SNAKE_IN_GGG(Pattern, Cols, Rows) → INFINITE_SNAKE_IN_GAA(Pattern, InfSnake, InfSnake)
INFINITE_SNAKE_IN_GAA(.(A, R), .(A, T), S) → U8_GAA(A, R, T, S, infinite_snake_in_gaa(R, T, S))
INFINITE_SNAKE_IN_GAA(.(A, R), .(A, T), S) → INFINITE_SNAKE_IN_GAA(R, T, S)
U5_GGG(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_GGG(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
U5_GGG(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → PRODUCE_SNAKE_IN_GGAA(Rows, Cols, InfSnake, Snake)
PRODUCE_SNAKE_IN_GGAA(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
PRODUCE_SNAKE_IN_GGAA(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → PART_OF_SNAKE_IN_GAAA(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_IN_GAAA(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_GAAA(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
PART_OF_SNAKE_IN_GAAA(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → PART_OF_SNAKE_IN_GAAA(R, Rings, RestSnake, RestRings)
U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_GGAA(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN_GGAA(Rows, Cols, NewInfSnake, Tail)
U6_GGG(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_GGG(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
U6_GGG(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → COIL_IT_IN_GG(Snake, odd)
COIL_IT_IN_GG(.(Line, Lines), odd) → U12_GG(Line, Lines, coil_it_in_gg(Lines, even))
COIL_IT_IN_GG(.(Line, Lines), odd) → COIL_IT_IN_GG(Lines, even)
COIL_IT_IN_GG(.(Line, Lines), even) → U13_GG(Line, Lines, reverse2_in_aa(Line, Line1))
COIL_IT_IN_GG(.(Line, Lines), even) → REVERSE2_IN_AA(Line, Line1)
REVERSE2_IN_AA(List, Reversed) → U15_AA(List, Reversed, reverse_in_aga(List, [], Reversed))
REVERSE2_IN_AA(List, Reversed) → REVERSE_IN_AGA(List, [], Reversed)
REVERSE_IN_AGA(.(Head, Tail), SoFar, Reversed) → U16_AGA(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
REVERSE_IN_AGA(.(Head, Tail), SoFar, Reversed) → REVERSE_IN_AGA(Tail, .(Head, SoFar), Reversed)
U13_GG(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_GG(Line, Lines, coil_it_in_gg(Lines, odd))
U13_GG(Line, Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_GG(Lines, odd)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg
S2L_IN_GA(x1, x2)  =  S2L_IN_GA(x1)
TEST_SNAKE_IN_GGG(x1, x2, x3)  =  TEST_SNAKE_IN_GGG(x1, x2, x3)
U10_GGAA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GGAA(x7)
INFINITE_SNAKE_IN_GAA(x1, x2, x3)  =  INFINITE_SNAKE_IN_GAA(x1)
U12_GG(x1, x2, x3)  =  U12_GG(x3)
REVERSE_IN_AGA(x1, x2, x3)  =  REVERSE_IN_AGA(x2)
U1_GGG(x1, x2, x3, x4)  =  U1_GGG(x1, x3, x4)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x4)
U3_GGG(x1, x2, x3, x4)  =  U3_GGG(x4)
REVERSE2_IN_AA(x1, x2)  =  REVERSE2_IN_AA
U16_AGA(x1, x2, x3, x4, x5)  =  U16_AGA(x5)
U9_GGAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GGAA(x2, x3, x7)
SNAKE_IN_GGG(x1, x2, x3)  =  SNAKE_IN_GGG(x1, x2, x3)
U5_GGG(x1, x2, x3, x4)  =  U5_GGG(x2, x3, x4)
PRODUCE_SNAKE_IN_GGAA(x1, x2, x3, x4)  =  PRODUCE_SNAKE_IN_GGAA(x1, x2)
U8_GAA(x1, x2, x3, x4, x5)  =  U8_GAA(x5)
U7_GGG(x1, x2, x3, x4)  =  U7_GGG(x4)
U13_GG(x1, x2, x3)  =  U13_GG(x2, x3)
U2_GGG(x1, x2, x3, x4, x5)  =  U2_GGG(x1, x4, x5)
U15_AA(x1, x2, x3)  =  U15_AA(x3)
U14_GG(x1, x2, x3)  =  U14_GG(x3)
COIL_IT_IN_GG(x1, x2)  =  COIL_IT_IN_GG(x1, x2)
U11_GAAA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GAAA(x7)
U6_GGG(x1, x2, x3, x4)  =  U6_GGG(x4)
PART_OF_SNAKE_IN_GAAA(x1, x2, x3, x4)  =  PART_OF_SNAKE_IN_GAAA(x1)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

TEST_SNAKE_IN_GGG(Pattern, C, R) → U1_GGG(Pattern, C, R, s2l_in_ga(C, Cols))
TEST_SNAKE_IN_GGG(Pattern, C, R) → S2L_IN_GA(C, Cols)
S2L_IN_GA(s(X), .(X1, Y)) → U4_GA(X, X1, Y, s2l_in_ga(X, Y))
S2L_IN_GA(s(X), .(X1, Y)) → S2L_IN_GA(X, Y)
U1_GGG(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_GGG(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U1_GGG(Pattern, C, R, s2l_out_ga(C, Cols)) → S2L_IN_GA(R, Rows)
U2_GGG(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_GGG(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
U2_GGG(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → SNAKE_IN_GGG(Pattern, Cols, Rows)
SNAKE_IN_GGG(Pattern, Cols, Rows) → U5_GGG(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
SNAKE_IN_GGG(Pattern, Cols, Rows) → INFINITE_SNAKE_IN_GAA(Pattern, InfSnake, InfSnake)
INFINITE_SNAKE_IN_GAA(.(A, R), .(A, T), S) → U8_GAA(A, R, T, S, infinite_snake_in_gaa(R, T, S))
INFINITE_SNAKE_IN_GAA(.(A, R), .(A, T), S) → INFINITE_SNAKE_IN_GAA(R, T, S)
U5_GGG(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_GGG(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
U5_GGG(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → PRODUCE_SNAKE_IN_GGAA(Rows, Cols, InfSnake, Snake)
PRODUCE_SNAKE_IN_GGAA(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
PRODUCE_SNAKE_IN_GGAA(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → PART_OF_SNAKE_IN_GAAA(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_IN_GAAA(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_GAAA(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
PART_OF_SNAKE_IN_GAAA(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → PART_OF_SNAKE_IN_GAAA(R, Rings, RestSnake, RestRings)
U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_GGAA(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN_GGAA(Rows, Cols, NewInfSnake, Tail)
U6_GGG(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_GGG(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
U6_GGG(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → COIL_IT_IN_GG(Snake, odd)
COIL_IT_IN_GG(.(Line, Lines), odd) → U12_GG(Line, Lines, coil_it_in_gg(Lines, even))
COIL_IT_IN_GG(.(Line, Lines), odd) → COIL_IT_IN_GG(Lines, even)
COIL_IT_IN_GG(.(Line, Lines), even) → U13_GG(Line, Lines, reverse2_in_aa(Line, Line1))
COIL_IT_IN_GG(.(Line, Lines), even) → REVERSE2_IN_AA(Line, Line1)
REVERSE2_IN_AA(List, Reversed) → U15_AA(List, Reversed, reverse_in_aga(List, [], Reversed))
REVERSE2_IN_AA(List, Reversed) → REVERSE_IN_AGA(List, [], Reversed)
REVERSE_IN_AGA(.(Head, Tail), SoFar, Reversed) → U16_AGA(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
REVERSE_IN_AGA(.(Head, Tail), SoFar, Reversed) → REVERSE_IN_AGA(Tail, .(Head, SoFar), Reversed)
U13_GG(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_GG(Line, Lines, coil_it_in_gg(Lines, odd))
U13_GG(Line, Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_GG(Lines, odd)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg
S2L_IN_GA(x1, x2)  =  S2L_IN_GA(x1)
TEST_SNAKE_IN_GGG(x1, x2, x3)  =  TEST_SNAKE_IN_GGG(x1, x2, x3)
U10_GGAA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GGAA(x7)
INFINITE_SNAKE_IN_GAA(x1, x2, x3)  =  INFINITE_SNAKE_IN_GAA(x1)
U12_GG(x1, x2, x3)  =  U12_GG(x3)
REVERSE_IN_AGA(x1, x2, x3)  =  REVERSE_IN_AGA(x2)
U1_GGG(x1, x2, x3, x4)  =  U1_GGG(x1, x3, x4)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x4)
U3_GGG(x1, x2, x3, x4)  =  U3_GGG(x4)
REVERSE2_IN_AA(x1, x2)  =  REVERSE2_IN_AA
U16_AGA(x1, x2, x3, x4, x5)  =  U16_AGA(x5)
U9_GGAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GGAA(x2, x3, x7)
SNAKE_IN_GGG(x1, x2, x3)  =  SNAKE_IN_GGG(x1, x2, x3)
U5_GGG(x1, x2, x3, x4)  =  U5_GGG(x2, x3, x4)
PRODUCE_SNAKE_IN_GGAA(x1, x2, x3, x4)  =  PRODUCE_SNAKE_IN_GGAA(x1, x2)
U8_GAA(x1, x2, x3, x4, x5)  =  U8_GAA(x5)
U7_GGG(x1, x2, x3, x4)  =  U7_GGG(x4)
U13_GG(x1, x2, x3)  =  U13_GG(x2, x3)
U2_GGG(x1, x2, x3, x4, x5)  =  U2_GGG(x1, x4, x5)
U15_AA(x1, x2, x3)  =  U15_AA(x3)
U14_GG(x1, x2, x3)  =  U14_GG(x3)
COIL_IT_IN_GG(x1, x2)  =  COIL_IT_IN_GG(x1, x2)
U11_GAAA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GAAA(x7)
U6_GGG(x1, x2, x3, x4)  =  U6_GGG(x4)
PART_OF_SNAKE_IN_GAAA(x1, x2, x3, x4)  =  PART_OF_SNAKE_IN_GAAA(x1)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 6 SCCs with 23 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

REVERSE_IN_AGA(.(Head, Tail), SoFar, Reversed) → REVERSE_IN_AGA(Tail, .(Head, SoFar), Reversed)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg
REVERSE_IN_AGA(x1, x2, x3)  =  REVERSE_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

REVERSE_IN_AGA(.(Head, Tail), SoFar, Reversed) → REVERSE_IN_AGA(Tail, .(Head, SoFar), Reversed)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
REVERSE_IN_AGA(x1, x2, x3)  =  REVERSE_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Instantiation
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

REVERSE_IN_AGA(SoFar) → REVERSE_IN_AGA(.(SoFar))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule REVERSE_IN_AGA(SoFar) → REVERSE_IN_AGA(.(SoFar)) we obtained the following new rules:

REVERSE_IN_AGA(.(z0)) → REVERSE_IN_AGA(.(.(z0)))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Instantiation
                          ↳ QDP
                            ↳ Instantiation
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

REVERSE_IN_AGA(.(z0)) → REVERSE_IN_AGA(.(.(z0)))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule REVERSE_IN_AGA(.(z0)) → REVERSE_IN_AGA(.(.(z0))) we obtained the following new rules:

REVERSE_IN_AGA(.(.(z0))) → REVERSE_IN_AGA(.(.(.(z0))))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Instantiation
                          ↳ QDP
                            ↳ Instantiation
                              ↳ QDP
                                ↳ NonTerminationProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

REVERSE_IN_AGA(.(.(z0))) → REVERSE_IN_AGA(.(.(.(z0))))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

REVERSE_IN_AGA(.(.(z0))) → REVERSE_IN_AGA(.(.(.(z0))))

The TRS R consists of the following rules:none


s = REVERSE_IN_AGA(.(.(z0))) evaluates to t =REVERSE_IN_AGA(.(.(.(z0))))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from REVERSE_IN_AGA(.(.(z0))) to REVERSE_IN_AGA(.(.(.(z0)))).





↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

COIL_IT_IN_GG(.(Line, Lines), even) → U13_GG(Line, Lines, reverse2_in_aa(Line, Line1))
U13_GG(Line, Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_GG(Lines, odd)
COIL_IT_IN_GG(.(Line, Lines), odd) → COIL_IT_IN_GG(Lines, even)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg
U13_GG(x1, x2, x3)  =  U13_GG(x2, x3)
COIL_IT_IN_GG(x1, x2)  =  COIL_IT_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

COIL_IT_IN_GG(.(Line, Lines), even) → U13_GG(Line, Lines, reverse2_in_aa(Line, Line1))
U13_GG(Line, Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_GG(Lines, odd)
COIL_IT_IN_GG(.(Line, Lines), odd) → COIL_IT_IN_GG(Lines, even)

The TRS R consists of the following rules:

reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
[]  =  []
odd  =  odd
even  =  even
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U13_GG(x1, x2, x3)  =  U13_GG(x2, x3)
COIL_IT_IN_GG(x1, x2)  =  COIL_IT_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U13_GG(Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_GG(Lines, odd)
COIL_IT_IN_GG(.(Lines), odd) → COIL_IT_IN_GG(Lines, even)
COIL_IT_IN_GG(.(Lines), even) → U13_GG(Lines, reverse2_in_aa)

The TRS R consists of the following rules:

reverse2_in_aa → U15_aa(reverse_in_aga([]))
U15_aa(reverse_out_aga(List, Reversed)) → reverse2_out_aa(List, Reversed)
reverse_in_aga(Reversed) → reverse_out_aga([], Reversed)
reverse_in_aga(SoFar) → U16_aga(reverse_in_aga(.(SoFar)))
U16_aga(reverse_out_aga(Tail, Reversed)) → reverse_out_aga(.(Tail), Reversed)

The set Q consists of the following terms:

reverse2_in_aa
U15_aa(x0)
reverse_in_aga(x0)
U16_aga(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

PART_OF_SNAKE_IN_GAAA(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → PART_OF_SNAKE_IN_GAAA(R, Rings, RestSnake, RestRings)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg
PART_OF_SNAKE_IN_GAAA(x1, x2, x3, x4)  =  PART_OF_SNAKE_IN_GAAA(x1)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

PART_OF_SNAKE_IN_GAAA(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → PART_OF_SNAKE_IN_GAAA(R, Rings, RestSnake, RestRings)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
PART_OF_SNAKE_IN_GAAA(x1, x2, x3, x4)  =  PART_OF_SNAKE_IN_GAAA(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

PART_OF_SNAKE_IN_GAAA(.(R)) → PART_OF_SNAKE_IN_GAAA(R)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN_GGAA(Rows, Cols, NewInfSnake, Tail)
PRODUCE_SNAKE_IN_GGAA(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg
U9_GGAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GGAA(x2, x3, x7)
PRODUCE_SNAKE_IN_GGAA(x1, x2, x3, x4)  =  PRODUCE_SNAKE_IN_GGAA(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN_GGAA(Rows, Cols, NewInfSnake, Tail)
PRODUCE_SNAKE_IN_GGAA(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))

The TRS R consists of the following rules:

part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
[]  =  []
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x7)
U9_GGAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GGAA(x2, x3, x7)
PRODUCE_SNAKE_IN_GGAA(x1, x2, x3, x4)  =  PRODUCE_SNAKE_IN_GGAA(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U9_GGAA(Rows, Cols, part_of_snake_out_gaaa(Part)) → PRODUCE_SNAKE_IN_GGAA(Rows, Cols)
PRODUCE_SNAKE_IN_GGAA(.(Rows), Cols) → U9_GGAA(Rows, Cols, part_of_snake_in_gaaa(Cols))

The TRS R consists of the following rules:

part_of_snake_in_gaaa([]) → part_of_snake_out_gaaa([])
part_of_snake_in_gaaa(.(R)) → U11_gaaa(part_of_snake_in_gaaa(R))
U11_gaaa(part_of_snake_out_gaaa(RestRings)) → part_of_snake_out_gaaa(.(RestRings))

The set Q consists of the following terms:

part_of_snake_in_gaaa(x0)
U11_gaaa(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

INFINITE_SNAKE_IN_GAA(.(A, R), .(A, T), S) → INFINITE_SNAKE_IN_GAA(R, T, S)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg
INFINITE_SNAKE_IN_GAA(x1, x2, x3)  =  INFINITE_SNAKE_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

INFINITE_SNAKE_IN_GAA(.(A, R), .(A, T), S) → INFINITE_SNAKE_IN_GAA(R, T, S)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
INFINITE_SNAKE_IN_GAA(x1, x2, x3)  =  INFINITE_SNAKE_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

INFINITE_SNAKE_IN_GAA(.(R)) → INFINITE_SNAKE_IN_GAA(R)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

S2L_IN_GA(s(X), .(X1, Y)) → S2L_IN_GA(X, Y)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg
S2L_IN_GA(x1, x2)  =  S2L_IN_GA(x1)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

S2L_IN_GA(s(X), .(X1, Y)) → S2L_IN_GA(X, Y)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
S2L_IN_GA(x1, x2)  =  S2L_IN_GA(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

S2L_IN_GA(s(X)) → S2L_IN_GA(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:


We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
test_snake_in: (b,b,b)
s2l_in: (b,f)
snake_in: (b,b,b)
infinite_snake_in: (b,f,f)
produce_snake_in: (b,b,f,f)
part_of_snake_in: (b,f,f,f)
coil_it_in: (b,b)
reverse2_in: (f,f)
reverse_in: (f,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1, x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x1, x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x2, x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x1, x2, x3, x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x1, x2, x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x1, x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x2, x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x2, x3, x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x1, x2, x3, x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg(x1, x2)
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x2, x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x2, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x2, x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg(x1, x2, x3)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1, x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x1, x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x2, x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x1, x2, x3, x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x1, x2, x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x1, x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x2, x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x2, x3, x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x1, x2, x3, x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg(x1, x2)
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x2, x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x2, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x2, x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg(x1, x2, x3)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

TEST_SNAKE_IN_GGG(Pattern, C, R) → U1_GGG(Pattern, C, R, s2l_in_ga(C, Cols))
TEST_SNAKE_IN_GGG(Pattern, C, R) → S2L_IN_GA(C, Cols)
S2L_IN_GA(s(X), .(X1, Y)) → U4_GA(X, X1, Y, s2l_in_ga(X, Y))
S2L_IN_GA(s(X), .(X1, Y)) → S2L_IN_GA(X, Y)
U1_GGG(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_GGG(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U1_GGG(Pattern, C, R, s2l_out_ga(C, Cols)) → S2L_IN_GA(R, Rows)
U2_GGG(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_GGG(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
U2_GGG(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → SNAKE_IN_GGG(Pattern, Cols, Rows)
SNAKE_IN_GGG(Pattern, Cols, Rows) → U5_GGG(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
SNAKE_IN_GGG(Pattern, Cols, Rows) → INFINITE_SNAKE_IN_GAA(Pattern, InfSnake, InfSnake)
INFINITE_SNAKE_IN_GAA(.(A, R), .(A, T), S) → U8_GAA(A, R, T, S, infinite_snake_in_gaa(R, T, S))
INFINITE_SNAKE_IN_GAA(.(A, R), .(A, T), S) → INFINITE_SNAKE_IN_GAA(R, T, S)
U5_GGG(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_GGG(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
U5_GGG(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → PRODUCE_SNAKE_IN_GGAA(Rows, Cols, InfSnake, Snake)
PRODUCE_SNAKE_IN_GGAA(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
PRODUCE_SNAKE_IN_GGAA(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → PART_OF_SNAKE_IN_GAAA(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_IN_GAAA(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_GAAA(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
PART_OF_SNAKE_IN_GAAA(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → PART_OF_SNAKE_IN_GAAA(R, Rings, RestSnake, RestRings)
U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_GGAA(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN_GGAA(Rows, Cols, NewInfSnake, Tail)
U6_GGG(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_GGG(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
U6_GGG(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → COIL_IT_IN_GG(Snake, odd)
COIL_IT_IN_GG(.(Line, Lines), odd) → U12_GG(Line, Lines, coil_it_in_gg(Lines, even))
COIL_IT_IN_GG(.(Line, Lines), odd) → COIL_IT_IN_GG(Lines, even)
COIL_IT_IN_GG(.(Line, Lines), even) → U13_GG(Line, Lines, reverse2_in_aa(Line, Line1))
COIL_IT_IN_GG(.(Line, Lines), even) → REVERSE2_IN_AA(Line, Line1)
REVERSE2_IN_AA(List, Reversed) → U15_AA(List, Reversed, reverse_in_aga(List, [], Reversed))
REVERSE2_IN_AA(List, Reversed) → REVERSE_IN_AGA(List, [], Reversed)
REVERSE_IN_AGA(.(Head, Tail), SoFar, Reversed) → U16_AGA(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
REVERSE_IN_AGA(.(Head, Tail), SoFar, Reversed) → REVERSE_IN_AGA(Tail, .(Head, SoFar), Reversed)
U13_GG(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_GG(Line, Lines, coil_it_in_gg(Lines, odd))
U13_GG(Line, Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_GG(Lines, odd)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1, x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x1, x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x2, x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x1, x2, x3, x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x1, x2, x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x1, x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x2, x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x2, x3, x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x1, x2, x3, x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg(x1, x2)
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x2, x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x2, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x2, x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg(x1, x2, x3)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)
S2L_IN_GA(x1, x2)  =  S2L_IN_GA(x1)
TEST_SNAKE_IN_GGG(x1, x2, x3)  =  TEST_SNAKE_IN_GGG(x1, x2, x3)
U10_GGAA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GGAA(x2, x3, x7)
INFINITE_SNAKE_IN_GAA(x1, x2, x3)  =  INFINITE_SNAKE_IN_GAA(x1)
U12_GG(x1, x2, x3)  =  U12_GG(x2, x3)
REVERSE_IN_AGA(x1, x2, x3)  =  REVERSE_IN_AGA(x2)
U1_GGG(x1, x2, x3, x4)  =  U1_GGG(x1, x2, x3, x4)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x4)
U3_GGG(x1, x2, x3, x4)  =  U3_GGG(x1, x2, x3, x4)
REVERSE2_IN_AA(x1, x2)  =  REVERSE2_IN_AA
U16_AGA(x1, x2, x3, x4, x5)  =  U16_AGA(x3, x5)
U9_GGAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GGAA(x2, x3, x7)
SNAKE_IN_GGG(x1, x2, x3)  =  SNAKE_IN_GGG(x1, x2, x3)
U5_GGG(x1, x2, x3, x4)  =  U5_GGG(x1, x2, x3, x4)
PRODUCE_SNAKE_IN_GGAA(x1, x2, x3, x4)  =  PRODUCE_SNAKE_IN_GGAA(x1, x2)
U8_GAA(x1, x2, x3, x4, x5)  =  U8_GAA(x2, x5)
U7_GGG(x1, x2, x3, x4)  =  U7_GGG(x1, x2, x3, x4)
U13_GG(x1, x2, x3)  =  U13_GG(x2, x3)
U2_GGG(x1, x2, x3, x4, x5)  =  U2_GGG(x1, x2, x3, x4, x5)
U15_AA(x1, x2, x3)  =  U15_AA(x3)
U14_GG(x1, x2, x3)  =  U14_GG(x2, x3)
COIL_IT_IN_GG(x1, x2)  =  COIL_IT_IN_GG(x1, x2)
U11_GAAA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GAAA(x2, x7)
U6_GGG(x1, x2, x3, x4)  =  U6_GGG(x1, x2, x3, x4)
PART_OF_SNAKE_IN_GAAA(x1, x2, x3, x4)  =  PART_OF_SNAKE_IN_GAAA(x1)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

TEST_SNAKE_IN_GGG(Pattern, C, R) → U1_GGG(Pattern, C, R, s2l_in_ga(C, Cols))
TEST_SNAKE_IN_GGG(Pattern, C, R) → S2L_IN_GA(C, Cols)
S2L_IN_GA(s(X), .(X1, Y)) → U4_GA(X, X1, Y, s2l_in_ga(X, Y))
S2L_IN_GA(s(X), .(X1, Y)) → S2L_IN_GA(X, Y)
U1_GGG(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_GGG(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U1_GGG(Pattern, C, R, s2l_out_ga(C, Cols)) → S2L_IN_GA(R, Rows)
U2_GGG(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_GGG(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
U2_GGG(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → SNAKE_IN_GGG(Pattern, Cols, Rows)
SNAKE_IN_GGG(Pattern, Cols, Rows) → U5_GGG(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
SNAKE_IN_GGG(Pattern, Cols, Rows) → INFINITE_SNAKE_IN_GAA(Pattern, InfSnake, InfSnake)
INFINITE_SNAKE_IN_GAA(.(A, R), .(A, T), S) → U8_GAA(A, R, T, S, infinite_snake_in_gaa(R, T, S))
INFINITE_SNAKE_IN_GAA(.(A, R), .(A, T), S) → INFINITE_SNAKE_IN_GAA(R, T, S)
U5_GGG(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_GGG(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
U5_GGG(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → PRODUCE_SNAKE_IN_GGAA(Rows, Cols, InfSnake, Snake)
PRODUCE_SNAKE_IN_GGAA(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
PRODUCE_SNAKE_IN_GGAA(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → PART_OF_SNAKE_IN_GAAA(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_IN_GAAA(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_GAAA(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
PART_OF_SNAKE_IN_GAAA(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → PART_OF_SNAKE_IN_GAAA(R, Rings, RestSnake, RestRings)
U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_GGAA(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN_GGAA(Rows, Cols, NewInfSnake, Tail)
U6_GGG(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_GGG(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
U6_GGG(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → COIL_IT_IN_GG(Snake, odd)
COIL_IT_IN_GG(.(Line, Lines), odd) → U12_GG(Line, Lines, coil_it_in_gg(Lines, even))
COIL_IT_IN_GG(.(Line, Lines), odd) → COIL_IT_IN_GG(Lines, even)
COIL_IT_IN_GG(.(Line, Lines), even) → U13_GG(Line, Lines, reverse2_in_aa(Line, Line1))
COIL_IT_IN_GG(.(Line, Lines), even) → REVERSE2_IN_AA(Line, Line1)
REVERSE2_IN_AA(List, Reversed) → U15_AA(List, Reversed, reverse_in_aga(List, [], Reversed))
REVERSE2_IN_AA(List, Reversed) → REVERSE_IN_AGA(List, [], Reversed)
REVERSE_IN_AGA(.(Head, Tail), SoFar, Reversed) → U16_AGA(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
REVERSE_IN_AGA(.(Head, Tail), SoFar, Reversed) → REVERSE_IN_AGA(Tail, .(Head, SoFar), Reversed)
U13_GG(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_GG(Line, Lines, coil_it_in_gg(Lines, odd))
U13_GG(Line, Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_GG(Lines, odd)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1, x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x1, x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x2, x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x1, x2, x3, x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x1, x2, x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x1, x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x2, x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x2, x3, x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x1, x2, x3, x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg(x1, x2)
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x2, x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x2, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x2, x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg(x1, x2, x3)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)
S2L_IN_GA(x1, x2)  =  S2L_IN_GA(x1)
TEST_SNAKE_IN_GGG(x1, x2, x3)  =  TEST_SNAKE_IN_GGG(x1, x2, x3)
U10_GGAA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GGAA(x2, x3, x7)
INFINITE_SNAKE_IN_GAA(x1, x2, x3)  =  INFINITE_SNAKE_IN_GAA(x1)
U12_GG(x1, x2, x3)  =  U12_GG(x2, x3)
REVERSE_IN_AGA(x1, x2, x3)  =  REVERSE_IN_AGA(x2)
U1_GGG(x1, x2, x3, x4)  =  U1_GGG(x1, x2, x3, x4)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x4)
U3_GGG(x1, x2, x3, x4)  =  U3_GGG(x1, x2, x3, x4)
REVERSE2_IN_AA(x1, x2)  =  REVERSE2_IN_AA
U16_AGA(x1, x2, x3, x4, x5)  =  U16_AGA(x3, x5)
U9_GGAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GGAA(x2, x3, x7)
SNAKE_IN_GGG(x1, x2, x3)  =  SNAKE_IN_GGG(x1, x2, x3)
U5_GGG(x1, x2, x3, x4)  =  U5_GGG(x1, x2, x3, x4)
PRODUCE_SNAKE_IN_GGAA(x1, x2, x3, x4)  =  PRODUCE_SNAKE_IN_GGAA(x1, x2)
U8_GAA(x1, x2, x3, x4, x5)  =  U8_GAA(x2, x5)
U7_GGG(x1, x2, x3, x4)  =  U7_GGG(x1, x2, x3, x4)
U13_GG(x1, x2, x3)  =  U13_GG(x2, x3)
U2_GGG(x1, x2, x3, x4, x5)  =  U2_GGG(x1, x2, x3, x4, x5)
U15_AA(x1, x2, x3)  =  U15_AA(x3)
U14_GG(x1, x2, x3)  =  U14_GG(x2, x3)
COIL_IT_IN_GG(x1, x2)  =  COIL_IT_IN_GG(x1, x2)
U11_GAAA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GAAA(x2, x7)
U6_GGG(x1, x2, x3, x4)  =  U6_GGG(x1, x2, x3, x4)
PART_OF_SNAKE_IN_GAAA(x1, x2, x3, x4)  =  PART_OF_SNAKE_IN_GAAA(x1)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 6 SCCs with 23 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

REVERSE_IN_AGA(.(Head, Tail), SoFar, Reversed) → REVERSE_IN_AGA(Tail, .(Head, SoFar), Reversed)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1, x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x1, x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x2, x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x1, x2, x3, x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x1, x2, x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x1, x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x2, x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x2, x3, x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x1, x2, x3, x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg(x1, x2)
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x2, x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x2, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x2, x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg(x1, x2, x3)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)
REVERSE_IN_AGA(x1, x2, x3)  =  REVERSE_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

REVERSE_IN_AGA(.(Head, Tail), SoFar, Reversed) → REVERSE_IN_AGA(Tail, .(Head, SoFar), Reversed)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
REVERSE_IN_AGA(x1, x2, x3)  =  REVERSE_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Instantiation
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

REVERSE_IN_AGA(SoFar) → REVERSE_IN_AGA(.(SoFar))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule REVERSE_IN_AGA(SoFar) → REVERSE_IN_AGA(.(SoFar)) we obtained the following new rules:

REVERSE_IN_AGA(.(z0)) → REVERSE_IN_AGA(.(.(z0)))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Instantiation
                          ↳ QDP
                            ↳ Instantiation
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

REVERSE_IN_AGA(.(z0)) → REVERSE_IN_AGA(.(.(z0)))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By instantiating [15] the rule REVERSE_IN_AGA(.(z0)) → REVERSE_IN_AGA(.(.(z0))) we obtained the following new rules:

REVERSE_IN_AGA(.(.(z0))) → REVERSE_IN_AGA(.(.(.(z0))))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Instantiation
                          ↳ QDP
                            ↳ Instantiation
                              ↳ QDP
                                ↳ NonTerminationProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

REVERSE_IN_AGA(.(.(z0))) → REVERSE_IN_AGA(.(.(.(z0))))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

REVERSE_IN_AGA(.(.(z0))) → REVERSE_IN_AGA(.(.(.(z0))))

The TRS R consists of the following rules:none


s = REVERSE_IN_AGA(.(.(z0))) evaluates to t =REVERSE_IN_AGA(.(.(.(z0))))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from REVERSE_IN_AGA(.(.(z0))) to REVERSE_IN_AGA(.(.(.(z0)))).





↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

COIL_IT_IN_GG(.(Line, Lines), even) → U13_GG(Line, Lines, reverse2_in_aa(Line, Line1))
U13_GG(Line, Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_GG(Lines, odd)
COIL_IT_IN_GG(.(Line, Lines), odd) → COIL_IT_IN_GG(Lines, even)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1, x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x1, x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x2, x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x1, x2, x3, x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x1, x2, x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x1, x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x2, x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x2, x3, x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x1, x2, x3, x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg(x1, x2)
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x2, x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x2, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x2, x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg(x1, x2, x3)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)
U13_GG(x1, x2, x3)  =  U13_GG(x2, x3)
COIL_IT_IN_GG(x1, x2)  =  COIL_IT_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

COIL_IT_IN_GG(.(Line, Lines), even) → U13_GG(Line, Lines, reverse2_in_aa(Line, Line1))
U13_GG(Line, Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_GG(Lines, odd)
COIL_IT_IN_GG(.(Line, Lines), odd) → COIL_IT_IN_GG(Lines, even)

The TRS R consists of the following rules:

reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
[]  =  []
odd  =  odd
even  =  even
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x2, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U13_GG(x1, x2, x3)  =  U13_GG(x2, x3)
COIL_IT_IN_GG(x1, x2)  =  COIL_IT_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U13_GG(Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_GG(Lines, odd)
COIL_IT_IN_GG(.(Lines), odd) → COIL_IT_IN_GG(Lines, even)
COIL_IT_IN_GG(.(Lines), even) → U13_GG(Lines, reverse2_in_aa)

The TRS R consists of the following rules:

reverse2_in_aa → U15_aa(reverse_in_aga([]))
U15_aa(reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
reverse_in_aga(Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(SoFar) → U16_aga(SoFar, reverse_in_aga(.(SoFar)))
U16_aga(SoFar, reverse_out_aga(Tail, .(SoFar), Reversed)) → reverse_out_aga(.(Tail), SoFar, Reversed)

The set Q consists of the following terms:

reverse2_in_aa
U15_aa(x0)
reverse_in_aga(x0)
U16_aga(x0, x1)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

PART_OF_SNAKE_IN_GAAA(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → PART_OF_SNAKE_IN_GAAA(R, Rings, RestSnake, RestRings)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1, x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x1, x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x2, x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x1, x2, x3, x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x1, x2, x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x1, x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x2, x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x2, x3, x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x1, x2, x3, x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg(x1, x2)
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x2, x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x2, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x2, x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg(x1, x2, x3)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)
PART_OF_SNAKE_IN_GAAA(x1, x2, x3, x4)  =  PART_OF_SNAKE_IN_GAAA(x1)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

PART_OF_SNAKE_IN_GAAA(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → PART_OF_SNAKE_IN_GAAA(R, Rings, RestSnake, RestRings)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
PART_OF_SNAKE_IN_GAAA(x1, x2, x3, x4)  =  PART_OF_SNAKE_IN_GAAA(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

PART_OF_SNAKE_IN_GAAA(.(R)) → PART_OF_SNAKE_IN_GAAA(R)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN_GGAA(Rows, Cols, NewInfSnake, Tail)
PRODUCE_SNAKE_IN_GGAA(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1, x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x1, x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x2, x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x1, x2, x3, x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x1, x2, x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x1, x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x2, x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x2, x3, x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x1, x2, x3, x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg(x1, x2)
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x2, x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x2, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x2, x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg(x1, x2, x3)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)
U9_GGAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GGAA(x2, x3, x7)
PRODUCE_SNAKE_IN_GGAA(x1, x2, x3, x4)  =  PRODUCE_SNAKE_IN_GGAA(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN_GGAA(Rows, Cols, NewInfSnake, Tail)
PRODUCE_SNAKE_IN_GGAA(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_GGAA(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))

The TRS R consists of the following rules:

part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
[]  =  []
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x1, x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x2, x7)
U9_GGAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GGAA(x2, x3, x7)
PRODUCE_SNAKE_IN_GGAA(x1, x2, x3, x4)  =  PRODUCE_SNAKE_IN_GGAA(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U9_GGAA(Rows, Cols, part_of_snake_out_gaaa(Cols, Part)) → PRODUCE_SNAKE_IN_GGAA(Rows, Cols)
PRODUCE_SNAKE_IN_GGAA(.(Rows), Cols) → U9_GGAA(Rows, Cols, part_of_snake_in_gaaa(Cols))

The TRS R consists of the following rules:

part_of_snake_in_gaaa([]) → part_of_snake_out_gaaa([], [])
part_of_snake_in_gaaa(.(R)) → U11_gaaa(R, part_of_snake_in_gaaa(R))
U11_gaaa(R, part_of_snake_out_gaaa(R, RestRings)) → part_of_snake_out_gaaa(.(R), .(RestRings))

The set Q consists of the following terms:

part_of_snake_in_gaaa(x0)
U11_gaaa(x0, x1)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

INFINITE_SNAKE_IN_GAA(.(A, R), .(A, T), S) → INFINITE_SNAKE_IN_GAA(R, T, S)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1, x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x1, x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x2, x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x1, x2, x3, x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x1, x2, x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x1, x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x2, x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x2, x3, x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x1, x2, x3, x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg(x1, x2)
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x2, x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x2, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x2, x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg(x1, x2, x3)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)
INFINITE_SNAKE_IN_GAA(x1, x2, x3)  =  INFINITE_SNAKE_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

INFINITE_SNAKE_IN_GAA(.(A, R), .(A, T), S) → INFINITE_SNAKE_IN_GAA(R, T, S)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
INFINITE_SNAKE_IN_GAA(x1, x2, x3)  =  INFINITE_SNAKE_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

INFINITE_SNAKE_IN_GAA(.(R)) → INFINITE_SNAKE_IN_GAA(R)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

S2L_IN_GA(s(X), .(X1, Y)) → S2L_IN_GA(X, Y)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, []) → s2l_out_ga(0, [])
s2l_in_ga(s(X), .(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), .(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_ggg(Pattern, Cols, Rows))
snake_in_ggg(Pattern, Cols, Rows) → U5_ggg(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa([], S, S) → infinite_snake_out_gaa([], S, S)
infinite_snake_in_gaa(.(A, R), .(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(.(A, R), .(A, T), S)
U5_ggg(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_ggg(Pattern, Cols, Rows, produce_snake_in_ggaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_ggaa([], X, X1, []) → produce_snake_out_ggaa([], X, X1, [])
produce_snake_in_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail)) → U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_gaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_gaaa([], RestSnake, RestSnake, []) → part_of_snake_out_gaaa([], RestSnake, RestSnake, [])
part_of_snake_in_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings)) → U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_gaaa(R, Rings, RestSnake, RestRings))
U11_gaaa(X, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_gaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_gaaa(.(X, R), .(Ring, Rings), RestSnake, .(Ring, RestRings))
U9_ggaa(X, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_gaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_ggaa(Rows, Cols, NewInfSnake, Tail))
U10_ggaa(X, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_ggaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_ggaa(.(X, Rows), Cols, InfSnake, .(Part, Tail))
U6_ggg(Pattern, Cols, Rows, produce_snake_out_ggaa(Rows, Cols, InfSnake, Snake)) → U7_ggg(Pattern, Cols, Rows, coil_it_in_gg(Snake, odd))
coil_it_in_gg([], X) → coil_it_out_gg([], X)
coil_it_in_gg(.(Line, Lines), odd) → U12_gg(Line, Lines, coil_it_in_gg(Lines, even))
coil_it_in_gg(.(Line, Lines), even) → U13_gg(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, [], Reversed))
reverse_in_aga([], Reversed, Reversed) → reverse_out_aga([], Reversed, Reversed)
reverse_in_aga(.(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aga(Tail, .(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aga(Tail, .(Head, SoFar), Reversed)) → reverse_out_aga(.(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, [], Reversed)) → reverse2_out_aa(List, Reversed)
U13_gg(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_gg(Line, Lines, coil_it_in_gg(Lines, odd))
U14_gg(Line, Lines, coil_it_out_gg(Lines, odd)) → coil_it_out_gg(.(Line, Lines), even)
U12_gg(Line, Lines, coil_it_out_gg(Lines, even)) → coil_it_out_gg(.(Line, Lines), odd)
U7_ggg(Pattern, Cols, Rows, coil_it_out_gg(Snake, odd)) → snake_out_ggg(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_ggg(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1, x2)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x4, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_ggg(x1, x2, x3)  =  snake_in_ggg(x1, x2, x3)
U5_ggg(x1, x2, x3, x4)  =  U5_ggg(x1, x2, x3, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
[]  =  []
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x2, x5)
U6_ggg(x1, x2, x3, x4)  =  U6_ggg(x1, x2, x3, x4)
produce_snake_in_ggaa(x1, x2, x3, x4)  =  produce_snake_in_ggaa(x1, x2)
produce_snake_out_ggaa(x1, x2, x3, x4)  =  produce_snake_out_ggaa(x1, x2, x4)
U9_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_ggaa(x2, x3, x7)
part_of_snake_in_gaaa(x1, x2, x3, x4)  =  part_of_snake_in_gaaa(x1)
part_of_snake_out_gaaa(x1, x2, x3, x4)  =  part_of_snake_out_gaaa(x1, x4)
U11_gaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_gaaa(x2, x7)
U10_ggaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_ggaa(x2, x3, x7)
U7_ggg(x1, x2, x3, x4)  =  U7_ggg(x1, x2, x3, x4)
coil_it_in_gg(x1, x2)  =  coil_it_in_gg(x1, x2)
coil_it_out_gg(x1, x2)  =  coil_it_out_gg(x1, x2)
odd  =  odd
U12_gg(x1, x2, x3)  =  U12_gg(x2, x3)
even  =  even
U13_gg(x1, x2, x3)  =  U13_gg(x2, x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x1, x2, x3)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa(x1, x2)
U14_gg(x1, x2, x3)  =  U14_gg(x2, x3)
snake_out_ggg(x1, x2, x3)  =  snake_out_ggg(x1, x2, x3)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)
S2L_IN_GA(x1, x2)  =  S2L_IN_GA(x1)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

S2L_IN_GA(s(X), .(X1, Y)) → S2L_IN_GA(X, Y)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
S2L_IN_GA(x1, x2)  =  S2L_IN_GA(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

S2L_IN_GA(s(X)) → S2L_IN_GA(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: